| Definitions | Type, t  T, Id,  x:A. B(x), (x l), {x:A| B(x) }, x:A  B(x), <a,b>, a:A fp B(a), IdDeq, P   Q, x:A B(x), P & Q, P  Q, type List, S  T, f(a), Prop,  x:A. B(x), Dec(P), State(ds), AtomFree(T;x), deq-member(eq;x;L),  b, False, f(x), x dom(f), xdom(f). v=f(x) P(x;v), , s = t,  A,  b,  , a = b, Unit, left+right, 2of(t), 1of(t), source(l), lnk(k), destination(l), Void, tag(k),  x.A(x), x. t(x), f(x)?z, IdLnk, isrcv(k), R-state(R;i), f  g, A || B, R-Feasible(R), True, false, eqof(d), p  q, x : v, Normal(T), Normal(ds), es realizer ind Rrframe compseq tag def, es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, Knd, @loc: only members of L read x, @loc: k sends only on links in L, @loc: k writes only members of L, @loc precondition for a(v:T):P State(ds) v, DeclaredType(ds;x), sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc effect knd(v:T) x := f State(ds) v , only events in L send on lnk with tag, @loc only events in L change x:T, @loc x initially v:T, Realizer, Top, x,y. t(x;y), left right,  , {T}, P Q,  x:A. B(x) |
| Lemmas | fpf-empty wf, fpf-join wf, top wf, fpf-join-dom, fpf-join-ap-sq, es realizer-induction, Rnone wf, Rplus wf, fpf-all wf, fpf-dom wf, fpf-trivial-subtype-top, R-state wf, es realizer wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, decl-type wf, Rpre wf, fpf wf, Raframe wf, Rbframe wf, Rrframe wf, Knd wf, bor wf, eqof wf, bfalse wf, true wf, R-Feasible wf, R-compat wf, isrcv wf, IdLnk wf, fpf-cap wf, tagof wf, ldst wf, lnk wf, lsrc wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, false wf, assert wf, deq-member wf, atom-free wf, decl-state wf, decidable wf, assert-deq-member, id-deq wf, l member wf, Id wf |